#ifndef DPVERIFIER_MODEL_HPP
#define DPVERIFIER_MODEL_HPP

#include "network/network.hpp"
#include "pec.hpp"

#include <sylvan.h>
#include <sylvan_obj.hpp>
using namespace sylvan;

class Changes {
public:
    Changes();
    void insert(BDD &delta, Port * const oldPort, Port * const newPort);
    void clean();
    vector<unordered_map<Port*, unordered_map<Port*, BDD> > > deviceOldNewPort;
};

class Model {
public:
    Model(const Network &network);
    void insertMiniBatch(vector<Rule*> rules);
    void consumeChanges();
    int changeSize();
    int predicateSize();
private:
    BDD bit[32];
    void identifyChangesInsert(Rule *rule);
    Network network;
    Changes changes;
    unordered_map<PEC, BDD, PECHasher> predicates;
    unordered_map<Port*, unordered_set<PEC, PECHasher> > portToPECs;
};

#endif //DPVERIFIER_MODEL_HPP